a,b:rationals. ((a + -(a) + b) = b)  ((-(a) + a + b) = b) 

latex

Definitions	imon{i:l}, igrp{i:l}, t  T, iabgrp{i:l}, t.2, t.1, prop{i:l}, mon{i:l}, grp{i:l}, abgrp{i:l}, qadd_grp, grp_inv(g), grp_op(g), x f y, grp_car(g), P  Q, x:A. B(x)
Lemmas	abgrp wf, comm wf, grp inv wf, inverse wf, grp id wf, grp op wf, grp car wf, monoid p wf, qadd grp wf, iabgrp op inv assoc